Struct isotope::term::Pi[][src]

pub struct Pi { /* fields omitted */ }
Expand description

A dependent function type

Implementations

Create a new dependent function type without any type-checking

Create a new dependent function type annotated with a given type

Create a new dependent function type which automatically has the minimal universe type

Compute the form of a pi type

Compute the code for a dependent function type with the given parameter type, result, and type annotation

Compute the filter for a dependent function type with the given parameter type, result, and type annotation

Compute the flags for a dependent function type with the given parameter type, result, and type annotation

Get the parameter type of this pi type

Get the result type of this pi type

Construct a unary function type over a given type

Compute whether a dependent function type locally type-checks given an annotation

Compute whether a dependent function type locally type-checks given a universe

Locally type-check this term. Returns flags afterwards.

Trait Implementations

Returns a copy of the value. Read more

Performs copy-assignment from source. Read more

The type this conses to

Cons this term within a given context. Return None if already consed.

Convert this term to it’s own consed type

Get this term, but consed

Formats the value using the given formatter. Read more

Whether this term depends on a variable with a given index: if equiv is true, also consider larger variables in the same equivalence class

Get whether a term depends on a variable base <= variable <= ix Read more

Get the variable filter of this term

Get the free variable bound of this term

Feeds this value into the given Hasher. Read more

Feeds a slice of this type into the given Hasher. Read more

This method tests for self and other values to be equal, and is used by ==. Read more

This method tests for !=.

This method tests for self and other values to be equal, and is used by ==. Read more

This method tests for !=.

This method tests for self and other values to be equal, and is used by ==. Read more

This method tests for !=.

The type this substitutes to

Substitute this value recursively

Convert this object’s consed form to it’s substituted form

Shift this term’s variables with index >= base in a given context

Shift this term’s variables with index >= base in a given context

Substitute this term’s variables with index >= base down a variable in a given context

Compare this value to another within a given context

Recursively convert this term to an AST in a given context, without it’s annotation

Locally typecheck a term: note this is context-independent, without caching

Globally typecheck a term, i.e. typecheck all subterms, without caching

Typecheck this term’s annotation, without caching

Load this term’s current flags

Set this term’s flags. May cause errors if done incorrectly!

Locally typecheck a term: note this is context-independent.

Globally typecheck a term, i.e. typecheck all subterms and their variables

Variable typecheck a term, i.e. typecheck all subterms and their variables.

Typecheck this term’s annotation

Globally typecheck a term and it’s annotation, i.e. typecheck all subterms, annotation subterms, and their variables

Typecheck a term in a given context

Typecheck this term along with it’s variables

Whether this term might be type-checked

The type of value this is consed to

The type of value this is substituted to

Convert this term to a Term, without any consing

Get the type annotation of this term

Get the index of this term in a program graph. Return None if this term is unindexed

Get whether this term is a type

Get whether this term is a universe

Get whether this term is a function

Get whether this term is a dependent function type

Get whether this term is in “root form”

Coerce this term to another type, with type-checking

Convert this term to an annotation, with only rudimentary type-checking

Get whether this term is a subtype of another in a given context

Get the hash-code of this term Read more

Get the hash-code of this term if it was untyped Read more

Compare this term to another within a given context

Apply this value, as a dependent function type, to a given vector of arguments in a given context Returns None if there is no change. Pops off consumed arguments. Read more

Get the form of this term

Coerce this term to another type, with type-checking

Coerce this term to another type, with type-checking

Coerce this term to another type, with type-checking

Convert this term to an annotation, with only rudimentary type-checking

Convert this term to an annotation, with only rudimentary type-checking

Convert this term to an annotation, with only rudimentary type-checking

Get whether this term is a constant.

Get whether this term is a subtype of another in general

Cast this type into another in a given typing context

Get whether this term has a universe in all contexts

Get whether this term has a pi type in all contexts

Substitute this term’s variables recursively given a context

Substitute this term’s variables given a context

Shift this term’s variables with index >= base up by n in a given context

Shift this term’s variables with index >= base up by n in a given context

Compare this term to a term ID, within a given context

Cons this term within a given context. Return None if already consed.

Convert this term to a TermId within a given context

Get the type of this term, if any

Get the type of this term, if any

Get the transported type of this term, if any

Get the base type of this term, if any

Get the type of this term, if any

Apply this value, as a function, to a given vector of arguments in a given context Returns None if there is no change. Pops off consumed arguments. Read more

Convert this term to a TermId, without any consing

Clone this term to a TermId, without any consing

Clone this term to a TermId within a given context

Clone this term to a Term without any consing

Shallow cons a term directly into a context

Shallow cons a term directly into a context, cloning if necessary

Get whether this term is in head normal form

Get whether this term is in beta normal form

Get whether this term is in eta normal form

Convert this term to a normal form

Convert this term a normal form

Convert this term to a normal form, or reduce it up to n steps

Convert this term a normal form, or reduce it up to n steps

Convert this term to a normal form, or reduce it up to n steps

Convert this term a normal form, or reduce it up to n steps

Auto Trait Implementations

Blanket Implementations

Gets the TypeId of self. Read more

Immutably borrows from an owned value. Read more

Mutably borrows from an owned value. Read more

Borrow an optional value of type T

Hash this using a given hasher

Cons this term within a given context. Return None if already consed.

Get the type annotation of this term

Get the index of this term in an isotope program graph, if any

Get the hash-code of this term

Get whether this term is a type

Get whether this term is a universe

Get whether this term is in “root form”

Get whether this term is a subtype of another term in a given context

Get whether this term has a universe in all contexts

Get the untyped hash-code of this term

Get the variable filter of this term

Shift this term’s variables with index >= base up by n in a given context

Whether this term has a given variable dependency

Whether this term has a given variable dependency below ix and above base

Load this term’s flags

Set this term’s flags

Compare this term to another dynamic term

Convert this term to an Any

Compare this term to another

Compare this term to a term ID

Compare self to key and return true if they are equal.

Performs the conversion.

Performs the conversion.

The resulting type after obtaining ownership.

Creates owned data from borrowed data, usually by cloning. Read more

🔬 This is a nightly-only experimental API. (toowned_clone_into)

recently added

Uses borrowed data to replace owned data, usually by cloning. Read more

The type returned in the event of a conversion error.

Performs the conversion.

The type returned in the event of a conversion error.

Performs the conversion.